\begin{tabbing}
$\forall$\=$D$:Dsys, ${\it sched}$:(Id$\rightarrow$($\mathbb{N}\rightarrow$(IdLnk+Id)+Unit)), $v$:($i$:Id$\rightarrow$M($i$).state),\+
\\[0ex]${\it dec}$:($j$,$b$:Id$\rightarrow$M($j$).state$\rightarrow$(M($j$).da(locl($b$))+Unit)).
\-\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ (\=$\forall$$i$:Id.\+
\\[0ex](\=$\forall$$l$:IdLnk.\+
\\[0ex]destination($l$) $=$ $i$
\\[0ex]$\Rightarrow$ M(source($l$)) sends on link $l$
\\[0ex]$\Rightarrow$ \=isl(${\it sched}$($i$))\+
\\[0ex]\& ($\forall$$t$:$\mathbb{N}$. $\exists$${\it t'}$:$\mathbb{N}$. $t$$\leq$${\it t'}$ \& isl(outl(${\it sched}$($i$))(${\it t'}$)) \& outl(outl(${\it sched}$($i$))(${\it t'}$)) $=$ $l$))
\-\-\\[0ex]\& (\=$\forall$$a$:Id.\+
\\[0ex]$a$ in dom(M($i$).pre)
\\[0ex]$\Rightarrow$ \=isl(${\it sched}$($i$))\+
\\[0ex]\& (\=$\forall$$t$:$\mathbb{N}$.\+
\\[0ex]$\exists$${\it t'}$:$\mathbb{N}$. $t$$\leq$${\it t'}$ \& $\neg_{2}$isl(outl(${\it sched}$($i$))(${\it t'}$)) \& outr(outl(${\it sched}$($i$))(${\it t'}$)) $=$ $a$)))
\-\-\-\-\\[0ex]$\Rightarrow$ FairFifo
\end{tabbing}